SAT problem

Definition

Denote by $\mathtt{SAT}$ the set of all satisfiable CNF formulae.

(satisfiable meaning there is some assignment of variables such that the formula evaluates to TRUE)

𝚂𝙰𝚃∈𝐍𝐏\mathtt{SAT} \in \mathbf{NP} (see NP)
- as a proof of satisfiability may simply be a satisfying truth assignment
- however, not clear for formulas not in SAT, what a proof of unsatisfiability could be, answer could yield insight on NP =? coNP (unresolved)
$\mathtt{SAT}$ is NP-hard
Cook-Levin theorem states that 𝚂𝙰𝚃\mathtt{SAT} is NP-complete
- k-SAT is NP-complete for all $k\geq 3$
- however, 2SAT can be solved in $O(n+m)$ for $n$ variables, $m$ clauses
$\mathtt{SAT} \leq_p$ 3SAT (reduces in polynomial time)
By Fagin's theorem, ESO = NP, thus SAT may be represented by ESO
- $\exists$ (variables) such that CNF statement = true